\begin{tabbing}
$\forall$$g$:GrpSig.
\\[0ex]($\exists$\=$h$:OCMon\+
\\[0ex]$\exists$\=$f$:$\mid$$g$$\mid\rightarrow\mid$$h$$\mid$\+
\\[0ex](IsMonHomInj($g$;$h$;$f$)
\\[0ex]\& RelsIso($\mid$$g$$\mid$;$\mid$$h$$\mid$;$x$,$y$.$\uparrow$($x$ =$_{b}$ $y$);$x$,$y$.$\uparrow$($x$ =$_{b}$ $y$);$f$)
\\[0ex]\& RelsIso($\mid$$g$$\mid$;$\mid$$h$$\mid$;$x$,$y$.$\uparrow$($x$ $\leq_{b}$ $y$);$x$,$y$.$\uparrow$($x$ $\leq_{b}$ $y$);$f$)))
\-\-\\[0ex]$\Rightarrow$ ($g$ $\in$ OCMon)
\end{tabbing}